ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:ecl(ds; da). ecl-kinds(x)  (Knd List) 

latex

Definitions	x. t(x), x,y,z. t(x;y;z), x,y,z,w. t(x;y;z;w), x,y. t(x;y), ecl-kinds(x), t  T, x:A. B(x), x(s), x(s1,s2,s3), x(s1,s2,s3,s4), x(s1,s2)
Lemmas	Id wf, Knd wf, fpf wf, ecl wf, nat wf, append wf, bool wf, ma-valtype wf, decl-state wf, ecl ind wf